Nuprl Lemma : f-rank_wf 11,40

es:event_system{i:l}, e:es-E(es), x,free:Id.
es-dtype(es; loc(e); x; Id)  (f-rank{i:l}(xfreeese (:  )) 
latex


Definitionst  T, #$n, x:AB(x), A  B, a < b, void, x:AB(x), P  Q, False, A, {x:AB(x)} , , , <ab>, b, b, , s = t, prop{i:l}, x:A  B(x), inc-snd(p), loc(e), es-vartype(esix), P  Q, es-dtype(esixT), es-after(esxe), Type, inc-fst(p), eq_id(ab), left + right, P  Q, Unit, xt(x), let x = a in b(x), if b then t else f fi , EqDecider(T), event_system{i:l}, let x,y = A in B(x;y), t.1, es-E(es), atom{$n:n}, case b of inl(x) => s(x) | inr(y) => t(y), A c B, f(a), f-rank{i:l}(xfreeese), x.A(x), x changed before e, True, T, es-locl(esee'), x:AB(x), SWellFounded(R(x;y)), ge(ij), -n, n + m, n - m, id-deq, Id, (last change to x before e)
Lemmasge wf, nat properties, event system wf, es-locl-swellfnd, es-locl wf, es-E wf, changed wf, last-change wf, last-change-property, loc-last-change, id-deq wf, deq wf, es-dtype wf, ifthenelse wf, let wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-eq-id, eq id wf, inc-fst wf, false wf, es-after wf, es-vartype wf, es-loc wf, subtype rel self, Id wf, inc-snd wf, nat wf, bool wf, bnot wf, not wf, assert wf, le wf

origin